Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Update link to point to correct section #18208

Merged
merged 1 commit into from
Jul 14, 2023

Conversation

Sporarum
Copy link
Contributor

In the reference, in Erased Definitions, link pointed to the Inline page, even though the content is in Compile Time Operations

In the reference, in Erased Definitions, link pointed to the Inline page, even though the content is in Compile Time Operations
@nicolasstucki
Copy link
Contributor

Strange, GitHub is showing the Merge pull request button before all test have passed.

@nicolasstucki
Copy link
Contributor

It is also showing CI tests for push. This should not be happening.
Screenshot 2023-07-14 at 13 09 29

@nicolasstucki
Copy link
Contributor

This is because it was not a PR on the main branch. It was on language-reference-stable.

@nicolasstucki
Copy link
Contributor

I enabled Require status checks to pass before merging on language-reference-stable.

@nicolasstucki
Copy link
Contributor

@Sporarum the Sporarum-patch-1 branch should not have been created in the dotty repo. That is why we have the extra push CI jobs.

@nicolasstucki
Copy link
Contributor

I also noticed that we have Sporarum-patch-trait-params branch in the dotty repo. This should be moved to the dotty-staging repo or deleted.

@nicolasstucki nicolasstucki merged commit 02717b6 into language-reference-stable Jul 14, 2023
@nicolasstucki nicolasstucki deleted the Sporarum-patch-1 branch July 14, 2023 12:19
@Sporarum
Copy link
Contributor Author

Oh I see, I did not look at the github popup in detail, I did not even know I had the permission to create a branch here (and maybe I don't)

Here is a capture of a new one:
image

You'll note this UI does not seem to give me an option to create the branch in another repo

@Sporarum
Copy link
Contributor Author

Same thing happened with #17988
Which I why Sporarum-patch-trait-params still exists

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants